a, b:. CoPrime(a,b)  (gcd(a;b) ~ 1) 

latex

Definitions	x:A. B(x), t  T, gcd(a;b), CoPrime(a,b), P  Q, P & Q, P  Q, P  Q, GCD(a;b;y), a ~ b
Lemmas	assoced weakening, gcd p functionality wrt assoced, gcd unique, assoced wf, gcd p wf, gcd wf, gcd sat pred